A {\em table schema} is of the form $T(A_1, \dots, A_n)$, with
$T$ the table name and $A_i$ attribute names  for $i=1 \dots n$.
We will refer to a particular attribute $A$ by using the notation $T.A$.
Each attribute $A$ has an associated type ({\em integer}, {\em string}, \dots ) represented by $type(T.A)$.
In this paper we only consider {\em integer} types, although the inclusion of other data types will be considered in future work.

An {\em instance} of a table schema $T(A_1, \dots, A_n)$
will be represented as a finite multiset of functions (called rows)
 $\multi{\mu_1, \mu_2, ..., \mu_m}$ such that
$dom(\mu_i) = \{T.A_1,\dots, T.A_n \}$, and $\mu_i(T.A_j) \in type(T.A_j)$ for every $i=1, \dots, m$,
$j=1, \dots, n$.
Observe that we qualify the attribute names in the domain by table names.
This is done because in general we will be interested in rows that combine attributes from
different tables, usually as result of cartesian products.
In the following, it is useful to consider each attribute $T.A_i$ in $dom(\mu)$
as a logic variable, and  $\mu$ as a logic substitution.

The concatenation of two rows $\mu_1$, $\mu_2$ with disjoint domain is
defined as the union of both functions represented as $\mu_1 \odot \mu_2$.
Given a row $\mu$ and an expression $e$ we use the notation
$e\mu$ to represent the value obtained applying the substitution $\mu$ to $e$.

If $dom(\mu) = \{T.A_1, \dots, T.A_n \}$  and $\nu = {\{ U.A_1  \mapsto T.A_1, \dots, U.A_n \mapsto T.A_n \} }$ (i.e., $\nu$ is a table renaming)
we will use the notation $\mu^{U}$ to represent the substitution composition $\nu \circ \mu$.
 The previous concepts for concatenations and substitutions can be extended to multisets of rows in a natural way.
 For instance, given the multiset
 of rows $S$ and the row $\mu$, $S\mu$ represents the application of $\mu$
 to each  member of the multiset. Analogously, given two multisets $S_1$, $S_2$, we define
 $$
  S_1 \odot S_2  = \{ \nu \circ \mu \mid \nu \in S_1, \mu \in S_2\}
 $$
 which constitutes the natural representation of \emph{cartesian products} in relational databases.
 Observe that although our representation for rows is different from the representation used usually in relational databases (tuples), it is possible to define an isomorphism $\row{\cdot}$ between the two representations. If $R$ is a relation and $\mu \in R$ is defined as $\mu = \multi{T_1.A_1 \mapsto a_1, \dots T_n.A_n \mapsto a_n}$, then $\row{\mu} = (a_1, \dots, a_n)$ where the order in the tuple is the lexicographic order of the attribute names. In order to define the inverse transformation we assume that every relation has a well-defined schema with attribute names $(T_1.A_1, \dots, T_n.A_n)$ with the attribute name positions in lexicographic order. Obviously, if $R$ is either a table or a view, $T_i = R$ for
 $i=1 \dots n$, but in the case of queries we can assume different relation names as prefixes. Then, if $t=(a_1, \dots, a_n)$ is a tuple in $R$ we define $\row{\mu}^{-1} = {T_1.A_1 \mapsto a_1, \dots T_n.A_n \mapsto a_n}$. It can be checked that the transformation is distributive with respect to $\prod$ and $\odot$. This means that $\row{t_1 \times t_2}^{-1} = \row{t_1}^{-1} \odot \row{t_2}^{-1}$ and $\row{\mu_1 \odot \mu_2} = \row{\mu_1} \times \row{\mu_2}$.

 \begin{definition} SQL view and query syntax. \\ \label{def:syntax}
The general form of a view is: \ {\sf
create view V($A_1$, \dots, $A_n$) as \  $Q$},
with $Q$ a query and $V.A_1, \dots V.A_n$ the name of the view attributes.
Queries can be:

\begin{enumerate}
\item Basic queries
{\sf
\begin{tabular}{ll}
%\multicolumn{2}{l}{create view V($A_1$, \dots, $A_n$) As} \\
 \hspace*{1cm} Q = & select $e_1$, \dots, $e_n$ from $R_1\ B_1$ , \dots, $R_m \ B_m$  where $C$; \\
\end{tabular}
}\smallskip

\noindent with $R_j$ tables or views for $j=1 \dots m$, $e_i$, $i=1 \dots n$ expressions involving constants, predefined functions and attributes of the form
$B_j.A$, $1 \leq j \leq m$, and $A$ an attribute of $R_j$. The condition $C$ must have one of the following forms:

         $$C ::= \cod{false} \mid  \cod{true} \mid e_1 \diamond e_2 \mid  C_1\ \cod{ and }\ C_2 \mid  C_1\ \cod{ or }\ C_2 \mid  \cod{ not }\, C1 \mid \cod{exists(Q)}$$
        with $e_1, e_2$ arithmetic expressions,  $\diamond \in \{ =, <>, >, <, >=, <= \}$,  $C_1$, $C_2$ SQL conditions and $Q$ an SQL query.

In the rest of the paper the logic values \emph{true} and \emph{false} are represented respectively by $\top$ and $\bot$ in order to be distinguished from the SQL reserved words
\cod{true} and \cod{false}.

\item Unions of the form $Q_1$ \cod{union} $Q_2$, with $Q_1$ and $Q_2$ queries.

\item Intersections of the form $Q_1$ \cod{intersects} $Q_2$, with $Q_1$ and $Q_2$ queries.
\end{enumerate}
\end{definition}

A {\em database schema} $D$ is a tuple $(\mathcal{T},\mathcal{C}, \mathcal{V})$, where $\mathcal{T}$
is a finite set of tables, $\mathcal{C}$ a finite set of
database constraints and $\mathcal{V}$ a finite set of views.
A {\em database instance} $d$ of a database
schema is a set of table instances, one for each table in $\mathcal{T}$ verifying $\mathcal{C}$
(thus we only consider {\em valid instances}).
 To represent the instance of a table $T$ in a database instance $d$ we will use the notation $d(T)$.
 In this paper  \emph{primary key} and \emph{foreign key} constraints are considered. They can be formally  defined as follows:
\begin{definition} \label{def:pkandfk}
Let $D$ be a database schema and $d$ a database instance. Let $T$ be  a table in $D$ such that
$d(T) = \multi{\mu_1, \dots, \mu_n}$, then:
\begin{enumerate}
\item \label{def:sql:primary} If $T$ has a primary key constraint defined over the columns $C_1, \dots, C_p$, then we say that
     $d$ is a valid instance with respect to this constraint if for every $i=1 \dots n$ the logic formula
$$\bigwedge_{j=1, j\neq i}^n(\bigvee_{k=1}^p \mu_i(T.C_k) \neq \mu_j(T.C_k) )$$
holds (that is, it is evaluated to $\top$).
\item   If $T$ has a foreign key constraint for the columns $C_1, \dots, C_f $ referring the columns $C'_1,...C'_f$ from table $T_2$. Then suppose that $d(T_2) = \multi{\nu_1, \dots, \nu_{n'}}$. Then $d$ is a valid instance with respect to this foreign key if for every $\mu_i$, $i=1 \dots n$ the following logic formula holds:
$$ \bigvee_{j=1, j\neq i}^{n'}(\bigwedge_{k=1}^f  \mu_i(T.C_k) = \nu_j(T_2.C'_k) )$$
\end{enumerate}
\end{definition}
That is, in the case of the primary key we require that every pair of rows must differ in at least one attribute of the primary key.  In the case of the foreign key, every row  $\mu_i$ in $T$ requires the existence of another tuple $\nu_j$ in $T_2$ such that they have the same values over the attributes defining the primary case in each case.

A {\em symbolic
database instance} $d_s$ is a database instance whose rows can contain  logic variables.
We say that  $d_s$ is satisfied by a substitution $\mu$ when $(d_s\mu)$
is a database instance. $\mu$ must substitute  all the logic variables in $d_s$ by
domain values.

Next we present a small example that is used in the rest of the paper.

\begin{example} \label{ex:running}
A board game for multiple players. Players are included into the following table

{\small
\begin{verbatim}
create table player {  id int primary key   };
\end{verbatim}
}
The board can contain pieces from different players, but only one piece at each position. The board state is represented by the following table:

{\small
\begin{verbatim}
create table board {
  int x,
  int y,
  int id,
  primary key x,y;
  foreign key(id) references player(id);
  };
\end{verbatim}
}

\noindent where \cod{x, y} are the position in the board and \cod{id} the player identifier.

We are interested in detecting the \cod{id}s of the players that are still playing (that is, they have at least one piece on the board),
whose pieces are \emph{threatened}: for every piece of the player there is a piece of a different player which is either in the same \cod{x} or in the
same \cod{y}. The views defining such pieces are the following:

{\small
\begin{verbatim}
create view nowPlaying(id) as
  select p.id
  from player p
  where exists (select b.id from board b where b.id=p.id);

create view checked(id) as
  select p.id
  from player p
  where exists (select n.id from nowPlaying n where n.id = p.id) and
        not exists (select b1.id from board b1
                    where b1.id = p.id and
                          not exists
                         (select b2.id from board b2
                          where (b2.x - b1.x) * (b2.y-b1.y)=0 and
                                (b1.id <> b2.id)));
\end{verbatim}
}

\end{example}

The \emph{syntactic dependency tree} for a view, table or query $R$, with $R$ in the root of this tree, is defined as:
\begin{itemize}
\item If $R$ is a table it has no children.
\item If $R$ is a view the only child is the syntactic dependency tree of its associated query.
\item If $R$ is a query the children are the syntactic dependency trees of the relations occurring in the \cod{from} section, plus one child for each subquery occurring in the \cod{where} section.
\end{itemize}

Now we are ready to define our  SQL operational semantics (SOS for short).

\begin{definition} \label{def:sqlop}
Let $\mathcal{D}$ a relational database schema and   $d$ be an instance of $\mathcal{D}$. Then the
SQL operational semantics, $SOS(d)$ is defined as follows:
\begin{enumerate}
\item For any table $T$ defined in $\mathcal{D}$,  $\SQL{T,d} = d(T)$.


\item For any simple query $Q$

        {\sf
        \begin{tabular}{ll}
       % \multicolumn{2}{l}{create view V($A_1$, \dots, $A_n$) as} \\
        \qquad select $e_1$, \dots, $e_n$ from $R_1\ B_1$ , \dots, $R_m \ B_m$  where $C$;
        \end{tabular}
        }
        \noindent
        define:
        $$\SQL{Q,d}  = \{ s_Q(\mu) \mid
        \nu_1 \in \SQL{R_1,d}, \dots, \nu_m \in \SQL{R_m,d},  \mu = {\nu_1}^{B_1} \odot \cdots \odot {\nu_m}^{B_m}, \SQL{C\mu,d} \}$$
        where  $s_Q(\mu)$ = $\{Q.A_1 \mapsto (e_1 \mu), \dots, Q.A_n \mapsto (e_n \mu) \}$, and
        $\SQL{C,d}$ is defined as follows
        \begin{itemize}
        \item If $C \equiv \cod{false}$ then  $\SQL{C, d} = \bot$
        \item If $C \equiv \cod{true}$ then  $\SQL{C, d} = \top$
        \item If $C \equiv e$, with $e$ an arithmetic expression involving constants then
              $\SQL{C, d} = e$
        \item If $C \equiv e_1 \diamond e_2$, with  $\diamond$ a relational operator, then  $\SQL{C, d} = (\SQL{e_1, d} \diamond \SQL{e_2,d})$ .
        \item If $C \equiv C_1\ \cod{ and }\ C_2$ then $\SQL{C,d} = \SQL{C_1, d} \wedge \SQL{C_2,d}$
        \item If $C \equiv C_1\ \cod{ or }\ C_2$ then $\SQL{C, d} =\SQL{C_1, d} \vee \SQL{C_2, d}$
        \item If $C \equiv \cod{ not }\ C_1$ then $\SQL{C, d} = \neg \SQL{C, d}$
        \item If $C \equiv \cod{ exists }\ Q$ then $\SQL{C,d} = \SQL{Q, d} \neq \emptyset$

        \end{itemize}

\item If $Q$ is a view with attributes $A_1, \dots, A_n$ defined by a query of the form \cod{$Q_1$ union $Q_2$}, then $\SQL{Q,d} = \SQL{Q1,d} \cup \SQL{Q2,d}$ with $\cup$ the union multiset operator.


\item   Analogously, if $Q$ is of the form \cod{$Q_1$ intersection $Q_2$} then, $\SQL{\rel,d} = \SQL{Q1,d} \cap \SQL{Q2,d}$), with $\cap$ the intersection multiset operator.

\item For any view $V$ with definition \cod{create view V($E_1$, \dots, $E_n$) as Q},
   $\SQL{V,d} = \SQL{Q,d} \{V.E_1 \mapsto Q.A_1, \dots, V.E_n \mapsto Q.A_n\}$.

\end{enumerate}
\end{definition}
The following observations can be useful for understanding SOS. Queries are treated as anonymous views, and the name \cod{Q} is always given as table name to the rows in the result.
Analogously $A_i$ is always the name given to the i-th expression in the \cod{select} clause. This is useful for instance for ensuring that unions and intersections provide homogeneous rows, and  also for the renaming applied by views in the last item. The expression $(e_1 \diamond e_2)\mu$ in the second case represents the logic value $\top$ or $\bot$ obtained after replacing each attribute by its value in $\mu$ and
evaluating the relational expression in usual logic. In well-defined SQL queries all the attributes in the expressions correspond exactly to one attribute of a relation defined in the query.
Well-defined existential subqueries must verify that after replacing the external attributes by values they become well-defined queries. This property is exploited in the
definition used in the existential condition $C(\mu) = (\SQL{Q\mu,d} \neq \emptyset)$, which must be read as: first replace in $Q$ all the external attributes by their values, then obtain their semantics, and finally check whether the result is different from the empty multiset.

Using this definition we can define a {\em positive test-case} (PTC) for a view $V$ as a non-empty database instance $d$ such that
$\SQL{V} \neq \emptyset$.
In previous papers we have used ERA  \cite{Molina08}  as suitable operational semantics for SQL. However ERA does not allow existential subqueries, a key point of this work that is solved in SOS.
 Defining ERA
and the transformation of SQL into ERA is beyond the scope of this paper, and we only mention some of the basic operations:
\begin{itemize}
  \item Unions and intersections.  The union of $R$ and $S$, is a multiset $R \cup S$ in which the row $\mu$ occurs $n+m$ times. The intersection of $R$ and $S$, $R \cap S$, is a multiset in which the row $\mu$ occurs $min(n,m)$ times.
  \item Projection. The expression $\pi_{e_1 \mapsto A_1, \dots, e_n \mapsto A_n}(R)$
         produces a new relation producing for each row $\mu \in R$ a
         new row $\{A_1 \mapsto e_1\row{\mu}, \dots , A_n \mapsto e_n\row{\mu} \}$. That is, we substitute in each $e_i$ the attribute names by their values in $\mu$ and then evaluate $e_i$.
         The resulting multiset has the same number of rows as $R$.
  \item Selection.
        Denoted by $\sigma_C(R)$, where $C$ is the condition that must be satisfied for
        all rows in the result.
        The selection operator on multisets applies the selection condition to each row occurring in the
         multiset independently.
  \item Cartesian products. Denoted as $R \times S$, each row in the first relation is paired with each row in the
second relation.
   \item Renaming.
The expression $\rho_S(R)$ changes the name of the relation $R$ to $S$.

\end{itemize}


A sound requirement is that both ERA and SOS must define the same semantics over the common SQL fragment. This is important because ERA is assumed as the standard SQL semantics.

\begin{theorem}
Let $D$ be a database schema and $d$ a database instance. Let $R$ be  a relation in $D$ or a query defined over relations in $D$. Assume that the relations in the syntactic dependency tree of $R$ do include neither aggregates not existential subqueries.
Then $\eta \in \SQL{R,d}$ with cardinality $k$  iff $ \row{\eta}  \in ERA(R,d)$ with cardinality $k$.
\end{theorem}
\begin{proof}
Using induction on the depth of the syntactic dependency tree for $R$, and distinguishing cases depending on the form of $R$:

\noindent - $R$ is a query of the form
\cod{select $e_1$, \dots, $e_n$ from $R_1\ B_1$ , \dots, $R_m \ B_m$  where $C$;}, and $C$ does not contain subqueries.
Then according to Definition \ref{def:sqlop}

\begin{align}
\SQL{Q,d}  = \{ s_Q(\mu) \mid
        \nu_1 \in \SQL{R_1,d}, \dots, \nu_m \in \SQL{R_m,d},  \mu = {\nu_1}^{B_1} \odot \cdots \odot {\nu_m}^{B_m}, \SQL{C\mu,d} \}\label{demo:ERA:sql}
        \end{align}

        It is easy to check that in the case of conditions without subqueries $\SQL{C\mu,d} = C'\mu$ where $C'$
        is obtained from $C$ by replacing \cod{true} by $\top$, \cod{false} by $\bot$, \cod{and} by $\wedge$, \cod{or}
        by $\vee$ and \cod{not} by $\neg$. Analogously in ERA the query can expressed as:
        \begin{align}
         &&&
        ERA(Q,d) = \prod_{e_1 \mapsto Q.A_1, \dots, e_n \mapsto Q.A_1} \sigma_{C'} (\rho_{B_1}(ERA(R_1,d)) \times \dots \times \rho_{B_m}(ERA(R_m,d))) \label{demo:ERA:ERA}
        \end{align}
        with $C'$ defined as above.
Now assume that $\eta \in \SQL{Q,d}$ with cardinality $k$. This means that there exists $\mu_1, \dots, \mu_k$ such that
$\eta = s_Q(\mu_i)$ for $i=1 \dots k$. According to \ref{demo:ERA:sql} this implies that
    \begin{align}
     &&&\mu_i = {\nu^i_1}^{B_1} \odot \cdots \odot {\nu^i_m}^{B_m}, \textrm{ with } \nu^i_j \in  \SQL{R_j,d} \textrm{ for } j=1 \dots m \label{demo:ERA:nuij}
    \end{align}
     Then applying the induction hypothesis to \ref{demo:ERA:nuij} we have that $\row{\nu^i_j} \in  ERA(R_j,d)$ with the same cardinality for $i=1 \dots n, j = 1 \dots m$, which means that  $ \rho{\nu^i_j}^{B_j} \in \rho_{B_j}(ERA(R_j,d))$
     for $i=1 \dots n, j = 1 \dots m$, and therefore $\rho{\mu_i} \in (\rho_{B_1}(ERA(R_1,d)) \times \dots \times \rho_{B_m}(ERA(R_m,d)))$. From \ref{demo:ERA:sql} we have that $\SQL{C\mu,d} = C'\mu_i$ holds, which means that
     $\rho{\mu_i} \in \sigma_{C'} (\rho_{B_1}(ERA(R_1,d)) \times \dots \times \rho_{B_m}(ERA(R_m,d)))$. Finally,
     taking into account that
     $\eta = s_Q(\mu_i)$ for $i=1 \dots k$, and considering that
     $\row{\eta} = \row{s_Q(\mu_i)}$ = $\{Q.A_1 \mapsto (e_1 \row{\mu_i}), \dots, Q.A_n \mapsto (e_n \row{\mu_i}) \}$ = $\prod_{e_1 \mapsto Q.A_1, \dots, e_n \mapsto Q.A_1} (\row{\mu_i})$  we have from \ref{demo:ERA:ERA} that $\row{\eta} \in ERA(Q,d)$.




\end{proof} 